Nuprl Definition : es-frame 11,40

@i only L affect x:T
== es-dtype(esixT)
== c alle-at(esie.(((es-kind(ese L))  (es-after(esxe) = es-when(esxe)))) 
latex



clarification:

es-frame(es;i;L;x;T)
== es-dtype(esixT)
== c alle-at(es;
== c alle-at(i;
== c alle-at(e.(((es-kind(ese L  Knd))  (es-after(esxe) = es-when(esxe T))
== c alle-at(
latex


DefinitionsA c B, es-dtype(esixT), alle-at(esie.P(e)), P  Q, A, (x  l), es-kind(ese), Knd, s = t, es-after(esxe), es-when(esxe)
FDL editor aliaseses-frame

origin